|
''Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I'' ("On Formally Undecidable Propositions of Principia Mathematica and Related Systems I") is a paper in mathematical logic by Kurt Gödel. Dated November 17, 1930, it was originally published in German in the 1931 volume of ''Monatshefte für Mathematik.'' Several English translations have appeared in print, and the paper has been included in two collections of classic mathematical logic papers. The paper contains theorems that have many implications for consistency proofs in mathematics and techniques that Gödel invented to prove these theorems. == Outline and key results == (詳細はincompleteness theorems, which have had an enormous impact on the field of mathematical logic. These appear as theorems VI and XI, respectively, in the paper. In order to prove these results, Gödel introduced in this paper a method now known as Gödel numbering. In this method, each sentence and formal proof in first-order arithmetic is assigned a particular natural number. Gödel shows that many properties of these proofs can be defined within any theory of arithmetic that is strong enough to define the primitive recursive functions. (The contemporary terminology for recursive functions and primitive recursive functions had not yet been established when the paper was published; Gödel used the word ''rekursiv'' ("recursive") for what are now known as primitive recursive functions.) The method of Gödel numbering has since become common in mathematical logic. Because the method of Gödel numbering was novel, and to avoid any ambiguity, Gödel presented a list of 45 explicit formal definitions of primitive recursive functions and relations used to manipulate and test Gödel numbers. He used these to give an explicit definition of a formula Bew(''x'') that is true if and only if ''x'' is the Gödel number of a sentence φ and there exists a natural number that is the Gödel number of a proof of φ (The German word for proof is ''Beweis''). A second new technique invented by Gödel in this paper was the use of self-referential sentences. Gödel showed that the classical paradoxes of self-reference, such as "This statement is false," can be recast as self-referential formal sentences of arithmetic. Informally, the sentence employed to prove Gödel's first incompleteness theorem says "This statement is not provable." The fact that such self-reference can be expressed within arithmetic was not known until Gödel's paper appeared; independent work of Alfred Tarski on his indefinability theorem was conducted around the same time but not published until 1936. In footnote 48a, Gödel stated that a planned second part of the paper would establish a link between consistency proofs and type theory, but Gödel did not publish a second part of the paper before his death. His 1958 paper in ''Dialectica'' did, however, show how type theory can be used to give a consistency proof for arithmetic. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「On Formally Undecidable Propositions of Principia Mathematica and Related Systems」の詳細全文を読む スポンサード リンク
|